$\forall$$T$:Type, $L$:$T$ List, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$), $i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. ($L$ o $f$)[$i$] $=$ $L$[$f$($i$)] $\in$ $T$